Nuprl Lemma : d-world-state_wf
11,40
postcript
pdf
D
:Dsys,
i
:Id. d-world-state(
D
;
i
)
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
d-world-state(
D
;
i
)
Lemmas
ma-tst
wf
,
d-m
wf
,
action
wf
,
d-decl
wf
,
ma-msg
wf
,
lsrc
wf
,
mlnk
wf
d
,
Id
wf
,
dsys
wf
origin
D:Dsys, i:Id. d-world-state(D;i) 
Type D:Dsys, i:Id. d-world-state(D;i) Type x:A. B(x) T